use crate::disvec::DisVec;
use std::io;
use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering};
use std::sync::{Arc, Condvar, Mutex};
use std::thread;
use std::time::Instant;

// const VAR_NUM: usize = 256;
//
// type Lit = i32;
// type VarSeq = [Lit; VAR_NUM];
// type VarScr = [f64; VAR_NUM];

type LitMem = Vec<DisVec>;
type OptVec = Option<DisVec>;
mod disvec;

mod parse;
use parse::parse;

// type Lit = i32;
// type VarSeq = [Lit; VAR_NUM];
// type VarScr = [f64; VAR_NUM];
use lazy_static::lazy_static;

lazy_static! {
  static ref THNUM: Arc<AtomicUsize> = Arc::new(AtomicUsize::new(0)); // Example initial value
  static ref CONDS: Arc<(Mutex<()>, Condvar)> = Arc::new((Mutex::new(()), Condvar::new()));
  static ref SATIS: AtomicBool = AtomicBool::new(false);
}

// static THNUM: AtomicUsize = AtomicUsize::new(1);
// static COND: Condvar = Condvar::new();

#[derive(Clone)]
pub struct ProLit {
  lit: i32,
  lev: usize,
  ant: OptVec,
}

// impl ProLit {
//   fn new(lit: i32, lev: usize, ant: OptVec) -> Self {
//     Self { lit, lev, ant }
//   }
// }
//
type ProMem = Vec<ProLit>;

fn val(pro_mem: &ProMem, vec: &DisVec) -> (usize, i32) {
  let mut asn = DisVec::new();

  for p in pro_mem.iter() {
    asn.set(p.lit);
  }

  if asn.any(vec) {
    return (0, 1);
  }

  let una = vec.dex & !asn.dex;
  if let Some(dex) = una.first_one() {
    let res = (dex as i32) * if vec.pol[dex] { 1 } else { -1 };
    (una.count_ones(), res)
  } else {
    (0, 0)
  }
}

fn assign(pro_mem: &mut ProMem, lit: i32, lev: usize, ant: Option<DisVec>) {
  pro_mem.push(ProLit { lit, lev, ant });
}

fn prop(lit_mem: &LitMem, pro_mem: &mut ProMem, mut pro_top: usize, var_num: usize) -> OptVec {
  while pro_top < pro_mem.len() {
    for c in lit_mem.iter() {
      match val(pro_mem, c) {
        (0, 1) => continue,
        (0, _) => return Some(c.clone()),
        (1, res) => assign(pro_mem, res, pro_mem[pro_top].lev, Some(c.clone())),
        _ => {}
      }
    }
    pro_top += 1;
  }

  if pro_mem.len() == var_num {
    let conds_loc = Arc::clone(&CONDS);
    let (_, cond) = &*conds_loc;
    SATIS.store(true, Ordering::Relaxed);
    cond.notify_all();

    if SATIS.load(Ordering::Relaxed) {
      print!("v ");
      for p in pro_mem {
        print!("{} ", p.lit);
      }
      println!("0");
    }
  }

  None
}

fn karnaugh(var_num: usize, lit_mem: Arc<LitMem>, pro_mem: &mut Box<ProMem>, pro_top: usize) {
  let mut res = 0;
  // let mut learnt = DisVec::new();

  if SATIS.load(Ordering::Relaxed) {
    let conds_loc = Arc::clone(&CONDS);
    let (_, cond) = &*conds_loc;
    THNUM.fetch_sub(1, Ordering::SeqCst);
    cond.notify_all();
    return;
  }

  while res == 0 {
    if SATIS.load(Ordering::SeqCst) {
      let conds_loc = Arc::clone(&CONDS);
      let (_, cond) = &*conds_loc;
      THNUM.fetch_sub(1, Ordering::SeqCst);
      cond.notify_all();
      return;
    }

    let con = prop(&lit_mem, pro_mem, pro_top, var_num);

    if con.is_some() {
      res = 20;
    } else {
      let mut val_mem = DisVec::new();

      for p in pro_mem.iter() {
        val_mem.set(p.lit);
      }

      for nex in 1..=var_num {
        if !val_mem.dex[nex] {
          let mut neg_mem = Box::new((*pro_mem).clone());
          let nex_lev = if pro_mem.is_empty() {
            1
          } else {
            pro_mem.last().unwrap().lev + 1
          };

          assign(&mut *pro_mem, nex as i32, nex_lev, None);
          assign(&mut *neg_mem, -(nex as i32), nex_lev, None);

          {
            let conds_loc = Arc::clone(&CONDS);
            let (_, cond) = &*conds_loc;
            THNUM.fetch_add(1, Ordering::SeqCst);
            cond.notify_all();
          }

          let lit_mem_ptr = Arc::clone(&lit_mem);
          thread::spawn(move || karnaugh(var_num, lit_mem_ptr, &mut *neg_mem, pro_top));

          break;
        }
      }
    }
  }

  let conds_loc = Arc::clone(&CONDS);
  let (_, cond) = &*conds_loc;
  THNUM.fetch_sub(1, Ordering::SeqCst);
  cond.notify_all();
}

fn main() -> io::Result<()> {
  let args: Vec<String> = std::env::args().collect();
  println!("c file            {}", args[1]);

  let mut lit_mem = Arc::new(vec![]);
  let mut pro_mem: Box<Vec<ProLit>> = Box::new(vec![]);
  let mut var_num = 0;
  let mut cla_num = 0;

  let start = Instant::now();
  parse(
    &args[1],
    &mut Arc::get_mut(&mut lit_mem).unwrap(),
    &mut var_num,
    &mut cla_num,
  );

  let parse_duration = start.elapsed();
  println!("c elapse::parsing {}(us)", parse_duration.as_micros());
  println!("c VARS:           {}", var_num);

  // let pro_mem = Arc::new(Mutex::new(Vec::new()));
  // let lit_mem = Arc::new(lit_mem);

  karnaugh(var_num, lit_mem, &mut pro_mem, 0);
  {
    let conds_loc = Arc::clone(&CONDS);
    let (lock, cond) = &*conds_loc;
    cond
      .wait_while(lock.lock().unwrap(), |mut guard| {
        // println!("{}", THNUM.load(Ordering::SeqCst));
        THNUM.load(Ordering::SeqCst) != 0
      })
      .unwrap();
  }
  if SATIS.load(Ordering::SeqCst) {
    println!("s SAT");
  } else {
    println!("s UNSAT");
  }

  Ok(())
}
